(* # ===================================================================
   # Matrix Project
   # Copyright FEM-NUAA.CN 2020
   # =================================================================== *)


 (** ** Real MMatrix Module *)
Require Import Reals.
Open Scope R_scope.
Require Export Matrix.MMat.MMatrix_Module.
Require Export Matrix.Mat.RMatrix.
Require Import Matrix.Mat.RMtacs.


Module RMMatrix := MMatrix RM.

Definition RMMO := RMMatrix.MMO.

Definition RMMI := RMMatrix.MMI.

Definition RMMeq := @RMMatrix.MMeq.
Arguments RMMeq {m}{n}{m2}{n2}.

Definition RMMadd := @RMMatrix.MMadd.
Arguments RMMadd {m0}{n0}{m}{n}.

Definition RMMopp := @RMMatrix.MMopp.
Arguments RMMopp {m0}{n0}{m}{n}.

Definition RMMsub := @RMMatrix.MMsub.
Arguments RMMsub {m0}{n0}{m}{n}.

Definition RMMmult := @RMMatrix.MMmult.
Arguments RMMmult {m}{n}{p}{m2} {n2} {p2}.

Definition RMMadd_comm:=@RMMatrix.MMadd_comm.
Definition RMMadd_assoc:=@RMMatrix.MMadd_assoc.
Definition RMMadd_zero_l:=@RMMatrix.MMadd_zero_l.
Definition RMMadd_zero_r:=@RMMatrix.MMadd_zero_r.

Definition RMMsub_opp:=@RMMatrix.MMsub_opp.
Definition RMMsub_assoc:=@RMMatrix.MMsub_assoc.
Definition RMMsub_zero_l:=@RMMatrix.MMsub_zero_l.
Definition RMMsub_zero_r:=@RMMatrix.MMsub_zero_r.
Definition RMMsub_self:=@RMMatrix.MMsub_self.

Definition RMMmul_add_distr_l:= @RMMatrix.MMmul_add_distr_l.
Definition RMMmul_add_distr_r:= @RMMatrix.MMmul_add_distr_r.
Definition RMMmul_sub_distr_l:= @RMMatrix.MMmul_sub_distr_l.
Definition RMMmul_sub_distr_r:= @RMMatrix.MMmul_sub_distr_r.
Definition RMMmul_assoc:= @RMMatrix.MMmul_assoc.
Definition RMMmul_zero_l := @RMMatrix.MMmul_zero_l.
Definition RMMmul_zero_r := @RMMatrix.MMmul_zero_r.

Definition RMMtteq:= @RMMatrix.MMtteq.
Definition RMMtrans_add:= @RMMatrix.MMtrans_add.
Definition RMMtrans_sub:= @RMMatrix.MMtrans_sub.
Definition RMMtrans_mul:= @RMMatrix.MMtrans_mul.



